package alfabeta;

import net.sf.javabdd.BDD;
import net.sf.javabdd.BDDFactory;
import net.sf.javabdd.JFactory;

/**
 * 
 * This class build a BDD for the n-queen problem
 * The BDD is initialized with all the logical rules for the n-queen problem
 * All the logical rules are described in detail in the report attached this project.
 * 
 * @author jacobbj, jaje@itu.dk
 *
 */
public class NQueenBDD {

	private int size;
	public BDDFactory nqFact;
	public BoardIndex bddVarIndex; // array for keeping track of BDD variables
	public BDD queenRules; // BDD with n-queen rules
	private BDD True;
	private BDD False;

	public NQueenBDD(int size) {

		this.size = size;
		nqFact = JFactory.init(2000000, 200000); 
		nqFact.setVarNum(size*size);
		this.bddVarIndex = new BoardIndex(size);
		this.initialize(); // apply rules to BDD
	}

	// When a queen is added to the board, the corresponding variable is restricted to true
	public void addQueen(int col, int row) {

		this.queenRules = this.queenRules.restrict(this.nqFact.ithVar(this.bddVarIndex.getVarIndex(col, row)));

	}

	// Restricts a variable to false - used when invalid domains are found (unsat)
	public void setFalse (int varIndex) {

		// restrict field to False
		this.queenRules.restrict(this.nqFact.nithVar(varIndex));
		
	}
	
	// Tests if the BDD is satisfiable when a queen is added at the position of a variable
	public boolean isValid (int varIndex) {

		// restrict field to true
		BDD restricted = this.queenRules.restrict(this.nqFact.ithVar(varIndex));
		// return unsat?
		return restricted.isZero();
	}

	
	/**
	 * This method initializes the BDD for the n-queen problem
	 * It applies:
	 * 1) rules for one queen pr. row
	 * 2) rules for one queen pr. column
	 * 3) rules for at most one queen pr. diagonal
	 * ..see attached report for detailed description.
	 */
	private void initialize() {

		True = nqFact.one();
		False = nqFact.zero();

		// Build rule of one queen in each row
		// -----------------------------------
		this.queenRules = True;
		
		// iterate through all rows
		for (int row = 1; row <= size; row++) {
			
			BDD oneQueenInRow = False;

			// In each row - iterate through variables
			for (int var_index: bddVarIndex.varsInRow(row)) {

				// build expression for each variable true while all other false 
				BDD oneQueenAtIndex = True;
				for (int var: bddVarIndex.varsInRow(row)) {		
					if (var == var_index)
						oneQueenAtIndex = oneQueenAtIndex.and(nqFact.ithVar(var)); // x_i
					else
						oneQueenAtIndex = oneQueenAtIndex.and(nqFact.nithVar(var)); // NOT x_i
				}
				// combine expression of all indexes
				oneQueenInRow = oneQueenInRow.or(oneQueenAtIndex);
			}

			// add row rules to qeenRules
			queenRules = queenRules.and(oneQueenInRow);
		}

		// Build rule of one queen in each coumn
		// -----------------------------------
		
		// iterate through all columns
		for (int col = 1; col <= size; col++) {
			
			BDD oneQueenInColumn = False;

			// In each column - iterate through variables
			for (int var_index: bddVarIndex.varsInColumn(col)) {

				BDD oneQueenAtIndex = True;
				
				// build expression for each variable true while all other false
				for (int var: bddVarIndex.varsInColumn(col)) {		
					if (var == var_index)
						oneQueenAtIndex = oneQueenAtIndex.and(nqFact.ithVar(var)); // x_i
					else
						oneQueenAtIndex = oneQueenAtIndex.and(nqFact.nithVar(var)); // NOT x_i
				}

				// combine expression of all indexes
				oneQueenInColumn = oneQueenInColumn.or(oneQueenAtIndex);
			}

			// add column rules to queenRules
			queenRules = queenRules.and(oneQueenInColumn);
		}

		// ---------------------------------
		// add diagonal rules
		// no or max one queen in diagonals	
		// ----------------------------------
		
		// step 1: build from all diagonals right up in column 1
		int x = 1;
		
		// iterate through diagonals n column 1
		for (int y = size-1; y >=1; y--) {

			BDD noQueensInColumn = True;
			BDD maxOneQueenInColumn = False;
			
			// iterate through all variables in diagonal
			for (int i:bddVarIndex.varsRightDiagUp(x, y)) {

				// build expression of no queens
				noQueensInColumn = noQueensInColumn.and(nqFact.nithVar(i));
			} 

			// build expression for each variable true while all other false
			for (int i:bddVarIndex.varsRightDiagUp(x, y)) {

				BDD oneQueenAtIndex = True;
				// build expression of at most one queen
				for (int j: bddVarIndex.varsRightDiagUp(x, y)) {

					// one true and the rest false
					if (i == j) oneQueenAtIndex = oneQueenAtIndex.and(nqFact.ithVar(j));
					else oneQueenAtIndex = oneQueenAtIndex.and(nqFact.nithVar(j));		
				}

				// add rule for diagonal
				maxOneQueenInColumn = (maxOneQueenInColumn).or(oneQueenAtIndex);
			}

			// add to all diagonal rules
			BDD diagonalRule = (noQueensInColumn).or((maxOneQueenInColumn));	
			queenRules = queenRules.and(diagonalRule);
		}

		// step 2: build from all diagonals right up in column 2 to n-1
		int y = 1; // fix y
		
		// iterate through columns
		for (x = 2; x < size; x++) {

			BDD noQueensInColumn = True;
			BDD maxOneQueenInColumn = False;
			
			// iterate through variables in column
			for (int i:bddVarIndex.varsRightDiagUp(x, y)) {

				// build expression of no queens
				noQueensInColumn = noQueensInColumn.and(nqFact.nithVar(i));
			} 

			// build all rules for diagonal
			for (int i:bddVarIndex.varsRightDiagUp(x, y)) {

				BDD oneQueenAtIndex = True;
				// build expression of at most one queen
				for (int j: bddVarIndex.varsRightDiagUp(x, y)) {

					// one true and the rest false
					if (i == j) oneQueenAtIndex = oneQueenAtIndex.and(nqFact.ithVar(j));
					else oneQueenAtIndex = oneQueenAtIndex.and(nqFact.nithVar(j));		
				}
				maxOneQueenInColumn = (maxOneQueenInColumn).or(oneQueenAtIndex);
			}

			// add rules
			BDD diagonalRule = (noQueensInColumn).or((maxOneQueenInColumn));	
			queenRules = queenRules.and(diagonalRule);
		}

		// step 3: diagonals left up in column=size 
		x = size;
		for (y = size-1; y >=1; y--) {

			BDD noQueensInColumn = True;
			BDD maxOneQueenInColumn = False;
			for (int i:bddVarIndex.varsLeftDiagUp(x, y)) {

				// build expression of no queens
				noQueensInColumn = noQueensInColumn.and(nqFact.nithVar(i));
			} 

			for (int i:bddVarIndex.varsLeftDiagUp(x, y)) {

				BDD oneQueenAtIndex = True;
				// build expression of at most one queen
				for (int j: bddVarIndex.varsLeftDiagUp(x, y)) {

					// one true and the rest false
					if (i == j) oneQueenAtIndex = oneQueenAtIndex.and(nqFact.ithVar(j));
					else oneQueenAtIndex = oneQueenAtIndex.and(nqFact.nithVar(j));		
				}
				maxOneQueenInColumn = (maxOneQueenInColumn).or(oneQueenAtIndex);
			}

			BDD diagonalRule = (noQueensInColumn).or((maxOneQueenInColumn));	
			queenRules = queenRules.and(diagonalRule);
		}

		// step 4: diagonals left up in column 2 to column n
		y = 1;
		for (x = size-1; x > 1; x--) {

			BDD noQueensInColumn = True;
			BDD maxOneQueenInColumn = False;
			for (int i:bddVarIndex.varsLeftDiagUp(x, y)) {

				// build expression of no queens
				noQueensInColumn = noQueensInColumn.and(nqFact.nithVar(i));
			} 

			for (int i:bddVarIndex.varsLeftDiagUp(x, y)) {

				BDD oneQueenAtIndex = True;
				// build expression of at most one queen
				for (int j: bddVarIndex.varsLeftDiagUp(x, y)) {

					// one true and the rest false
					if (i == j) oneQueenAtIndex = oneQueenAtIndex.and(nqFact.ithVar(j));
					else oneQueenAtIndex = oneQueenAtIndex.and(nqFact.nithVar(j));		
				}
				maxOneQueenInColumn = (maxOneQueenInColumn).or(oneQueenAtIndex);
			}

			BDD diagonalRule = (noQueensInColumn).or((maxOneQueenInColumn));	
			queenRules = queenRules.and(diagonalRule);
		}		
	}
}
